Code and Notes (Week 2 Wednesday)

module ThirdLecture where

{-
  f(0) = 0
  f(n) = 2n - 1 + f(n-1)

  We want to prove:
    for all n: f(n) = n^2

  We can proceed by induction on n.
  (for P(n) = f(n) = n^2)

  Base case:
    prove: f(0) = 0^2

    f(0) =  (by definition)
    0 =
    0*0 = 0^2

  Inductive case:
    assuming f(n) = n^2 (IH)
    prove    f(n+1) = (n+1)^2

    f(n+1) = (by definition of f)
    2*(n+1) -1 + f(n) = (high-scool algebra)
    2*n + 2 - 1 + f(n) =  (high-scool algebra)
    2*n + 1 + f(n) = (by IH)
    2*n + 1 + n^2 = (by distributive law)
    (n+1)^2

  QED

  Note: the definition of f above is actually valid Haskell
 -}
f :: Int -> Int
f(0) = 0
f(n) = 2*n - 1 + f(n-1)
{- We started out by proving a closed form
   about a discrete math function.

   The discrete math function is valid Haskell,
   so we also verified (proved correct) a Haskell program!
    (caveat: we only proved it correct for non-negative inputs)
 -}

{- To reason about this function, we need to do something else.

   We *can* do induction on the length of the list arguments,
    but that's a bit clunky.

   We'd rather do induction on the list structure directly
   -- Structural induction (on lists)
 -}

{- What does _ mean?
   _ is a "wildcard pattern"
   *anything* matches an _

   Whenever you use _, you could have just put a fresh
    variable name there
   But with an _, you don't introduce a name for it
 -}

ones :: [Int]
ones = 1:ones

mymap :: (a -> b) -> [a] -> [b]
mymap _ [] = []
-- mymap f [] = []
mymap f (x:xs) = f x:mymap f xs

mylength [] = 0
mylength (x:xs) = 1 + mylength xs
{-
   for all xs: length(map f xs) = length xs

   By structural induction on xs

   Base case:
     length(map f []) = length []

     length(map f []) = (by def of map)
     length []          -- done

   Inductive case:
     Assuming IH: length(map f xs) = length xs
     Prove: length(map f (x:xs)) = length(x:xs)

     length(map f (x:xs)) = (by def of map)
     length(f x : map f xs) = (by def of length)
     1 + length(map f xs) = (by IH)
     1 + length(xs) = (by def of length backwards)
     length(x:xs)

   QED

 -}

--type Document = String

-- "Passport" represents a passport
-- "DriversLicence" represents a driver's licence

{-
points :: [Document] -> Int
points [] = 0
points ("Passport":xs) = 70 + points xs
 -}

{- This data representation is bad.
   I can represent *a lot* of things in Strings that aren't actually
   documents.

   What would be much nicer is to have a type that contains *only* ID documents

   the data keyword for the first time

   --- type keyword: introduces synonyms for existing types
   --- data keyword: introduces new types
 -}

data Document =
  Passport | BirthCertificate |
  DriversLicence | StudentID | CreditCard
  deriving (Eq,Show)
{- you can read this like an enum.

   Document is the name of the type that I'm defining
   the type as *constructors* separated by |
      Passport :: Document
      BirthCertificate :: Document

   crucially: the things I declare are the *only* Documents
 -}

isPrimary :: Document -> Bool
isPrimary Passport = True
isPrimary BirthCertificate = True
isPrimary _ = False

isSecondary DriversLicence = True
isSecondary StudentID = True
isSecondary _ = False

isTertiary CreditCard = True
isTertiary _ = False

points :: [Document] -> Int
points xs = 70*length primaries + 25*length tertiaries +
            secondaryPoints where
  primaries = filter isPrimary xs
  tertiaries = filter isTertiary xs
  secondaryPoints =
    case filter isSecondary xs of
      []   -> 0
      x:xs -> 40 + 25*length xs

{- By using a new type declared with data we:
   - eliminate malformed data from consideration
   - think about the bugs you cannot introduce
 -}

{- Q: could I define types in terms of other types?
   A: yes
 -}

data PrimaryDocument = Passportt | BirfCertificate
  deriving (Eq,Show)

data Documentt =
  Primary PrimaryDocument
  deriving (Eq,Show)


data MonthDay = MonthDay Int Int
  deriving (Eq,Show)
{- We are defining a *type* called MonthDay
   with a *constructor* called MonthDay
   -- that takes two *parameters*, an Int and an Int
 -}

getMonth :: MonthDay -> Int
getMonth (MonthDay month date) = month

data Coordinate = Coordinate Int Int
  deriving (Eq,Show)

{- Types with alternatives separated by | are sometimes called *sum
   types*

   Types with parameters to the constructor e.g.
       MonthDay n m are called *product types*
 -}

data MyMaybe a = MyNothing | MyJust a
  deriving (Eq,Show)
{- think: a principled way of saying
     "this is nullable"

   This type is often used to make
   partiality explicit and manageable
 -}

safeDiv :: Int -> Int -> Maybe Int
safeDiv _ 0 = Nothing
safeDiv n m = Just $ n `div` m

data NonEmpty a =
  One a
  | More a (NonEmpty a)

safeHead :: NonEmpty a -> a
safeHead(One a) = a
safeHead(More a _) = a

{- validate:
     check whether the input has a
     desirable property
        isPrimary
     the primary property is not captured
     by the type system
   parse:
     convert from a data representation
     with many failure states
     to one with fewer failure states
 -}

{- λ> :t show
  show :: Show a => a -> String

    For every type a that is an *instance*
      of Show,
    show has type a -> String

   Show here is a *type class*
   Type class is a set of types...
   ...with some operations that must be
      defined for every type in the class.
 -}

data Vegetable = Tomato | Carrot
  deriving Eq

instance Show Vegetable where
  show Tomato = "yuck!"
  show Carrot = "yum!"

{- Type class instances can take
   *constraints of their own*

instance Show a => Show [a] -- Defined in ‘GHC.Show’
 -}

class Sized a where
  size :: a -> Int

instance Sized Bool where
  size _ = 1

instance Sized Int where
  size _ = 1

instance Sized a => Sized [a] where
  size [] = 0
  size (x:xs) = size x + 1 + size xs
{-   ->  this is *function arrow*
    argument type on left
    return type on right

     => type on the right
        type class constraint
        on the left
 -}

{-  associative

      x * (y * z)  = (x * y) * z


    semigroups:
    -  the set of natural numbers,
       with addition
    -  the set of natural numbers,
       with multiplication
    -  the set of natural numbers,
       with min
    -  the set of natural numbers,
       with max
    -  the set of lists,
       with append (++)
    *non*-semigroup:
    -  the set of integers,
       with subtraction             
 -}

{-
instance (Semigroup a, Semigroup b) => Semigroup (a,b) where
  (a,b) <> (a',b') = (a<>a',b<>b')
-}

data Colour = Colour Int Int Int Int
  deriving (Eq,Show)

instance Semigroup Colour where
  Colour r g b t <> Colour r' g' b' t' =
    Colour (mix r r') (mix g g') (mix b b') (mix t t') where
    mix c c' = min 255 (c+c')

{- Is this associative?

   Claim: if mix is associative, then <> is also associative

     mix c (mix c' c'')   =   mix (mix c c') c''

     mix c (mix c' c'')   = (by definition)
     mix c (min 255 (c'+c'')) = (by definition)
     min 255 (c + (min 255 (c'+c''))) =
       (can't be bothered)

   If <> fails to be associative, this is called an
    *illegal instance*
   It would be a type class instance that doesn't satisfy the
   type class laws.

   We *can* write these, but shouldn't.
   We shouldn't because:
   - others will write code that assumes that the laws are valid
   - in some cases, the compiler could optimise your code in
     ways that only work for legal instances.
 -}

{-  Monoids are semigroups + an identity element 1 s.t.
           x*1 = x       1*x = x

    monoids:
    -  the set of natural numbers,
       with addition and identity element 0    x+0=0
    -  the set of natural numbers,
       with multiplication and identity element 1  x*1=x
    -  the set of natural numbers,
       with max with identity element 0  max x 0 = x
    -  the set of lists,
       with append (++) and identity []
    *non*-monoid:
    -  the set of integers,
       with subtraction
    -  the set of natural numbers,
       with min and... which identity element exactly?
    -  the set of integers,
       with max and... which identity element?
 -}

black = Colour 0 0 0 0

instance Monoid Colour where
  mempty  = black
  mappend = (<>)

-- mconcat [c1,c2,c3] = c1 `mappend` c2 `mappend` c3
-- mconcat [] = mempty

newtype Product = Product Int
  deriving (Show,Eq)

instance Semigroup Product where
  Product x <> Product y = Product(x*y)

instance Monoid Product where
  mempty = Product 1
  mappend = (<>)

{- I can use newtype when I have a datatype with exactly one
   constructor that only serves as a container.

   The main difference is performance-related:
   - Product (defined with newtype)
     will have the exact same runtime representation as
     Int
   - Product (defined with data)
     will be boxed
 -}

{- Usually, Eq instances are just syntactic equality.
   But you *can* imagine situations when you don't want that.

   Example:
     you might want to say that two binary search trees with
     the same elements, but different rotations, are equal


         3                1
        / \              /
       /   \            /
      1     5          3
                      /
                     /
                    5

  Moral: if you want to write this sort of instance,
   make sure you don't export the constructors,
   or indeed anything else that would allow you to tell them apart.
 -}